nLab three-sorted set theory

 Overview

Three-sorted set theories are set theories with three different sorts, representing sets, elements, and some third sort, usually functions or relations. Three-sorted set theories are usually structural set theories. In common with other simply sorted set theory, the membership $\in$ is a relation, in contrast to dependently sorted set theory, where membership is a typing judgment. In contrast to unsorted set theory and two-sorted set theory, sets and elements are different, and sets and elements are different from whatever relates sets and elements to each other (functions in categorical set theory, relations in allegorical set theory).

 Examples

• three-sorted SEAR

• three-sorted structural ZFC

• Similarly, there should be three-sorted presentations of ETCS with elements, although it has not been written out yet.

 See also

• unsorted set theory
• two-sorted set theory
• simply sorted set theory
• dependently sorted set theory